package automatica.upgrade;

import java.io.File;
import java.io.IOException;
import java.util.Hashtable;
import java.util.Vector;

import javax.swing.JOptionPane;

import prefuse.data.Table;
import ui.Utility;

public class TheoremGenerater1 {
	
	public TheoremGenerater1(String basicPath, String interPath, String advPath){
		
		//CMD --> INT
		
		InfoTable basicInfo = new InfoTable(fileLocate+basicPath);
		
		this.name = basicInfo.getName();
		
		basicInfo.countOccurence();	
		
		basicInfo.reasoning();
		
		basicInfo.removeRedundantObjects();
//		
//		
		basicInfo.print();
//		
		basicInfo.output(fileLocate+interPath);
		
		
		// INT --> GDL
		
		InfoTable advInfo = new InfoTable(fileLocate+advPath);
		advInfo.updateGeobject4ConstraintTable();
		
		
		Table basicTable = basicInfo.getObjectTable();
		this.objectTable = advInfo.getObjectTable();
		this.constraintTable = advInfo.getConstraintTable();
		
		//set label counts for advanced table
		for(int i = 0; i < basicTable.getRowCount(); i++){
			String label = basicTable.getString(i, "reference");
			for(int j = 0; j < objectTable.getRowCount(); j++){
				if(label.equals(objectTable.getString(j, "reference"))){
					objectTable.setInt(j, "pointCount", basicTable.getInt(i, "pointCount"));
				}
			}
		}
		
		advInfo.print();

		
		generateTheorem();
		advInfo.print();
		
		packageTheorem(fileLocate+advPath);
	
	}

	
	
	private void generateTheorem(){
		
		
		arrangeRelations();

		
		Vector<String> objects = new Vector<String>(1,1);
		for(int i = 0 ; i < objectTable.getRowCount(); i++){
			if(objectTable.getInt(i, "role")==1){
				String str = objectTable.getString(i, "reference")+":="+objectTable.getString(i, "geobject");
				objects.add(str);
			}
		}
		
		for(int i = relationList.size(); i > 0; i--){
			//select a relation to be conclusion
			//the conclusion only contains existing labels 
			Structure4Ordering currentR = relationList.get(i-1);
			boolean[] currentL = currentR.labelList;
			boolean currentCanBe = true;
			for(int k = 0; k < currentL.length; k++){
				if(currentL[k]==true){
					boolean test = false;
					for(int m = 0; m < relationList.size(); m++){
						if(m!=i-1){
							test = test || relationList.get(m).labelList[k];
						}
					}
					if(!test){
						currentCanBe = false;
					}
				}
			}
			
			//heuristics for the conclusions
			/*
			 * if an object is already constructed in the objectTable, then it can not be a conclusion unless there 
			 * are more than one constructions about the object
			 */
			if(currentR.tableName==objTab){
				String label = objectTable.getString(currentR.rowInTable,"reference");
				Vector<Integer> list = automatica.Utility.getRowNumList(objectTable, label, "reference");
				if(list.size()<=1){
					currentCanBe = false;
				}
			}
			
			
			if(currentCanBe){
				StringBuffer theorem = new StringBuffer(1);
				theorem.append("Problem(" + name +(i)+",Theorem,assume(");
				for(int k = 0; k < objects.size(); k++){
					theorem.append(objects.get(k)+",");
				}
				for(int j = 0; j < relationList.size(); j++){
					if(j!=i-1){
						Structure4Ordering so = relationList.get(j);
						if(so.tableName==objTab){
							theorem.append(objectTable.getString(so.rowInTable, "reference")+":="+objectTable.getString(so.rowInTable, "geobject")+",");
						}else
							if(so.tableName==conTab){
								theorem.append(constraintTable.getString(so.rowInTable, "geobject")+",");
							}
					}
				}
				
				String conclusion = "";
				Structure4Ordering conso = relationList.get(i-1);
				if(conso.tableName==objTab){
					if(objectTable.getInt(conso.rowInTable, "role")==2)
					conclusion = "is("+objectTable.getString(conso.rowInTable, "reference")+","+objectTable.getString(conso.rowInTable, "geobject")+")";
				}else
					if(conso.tableName==conTab){
						conclusion = constraintTable.getString(conso.rowInTable, "geobject");
					}
				
				theorem.replace(theorem.lastIndexOf(","), theorem.length(), "),show("+conclusion+"))");
				
				if(filterTheorem(theorem.toString())!=null){
					theorems.add(theorem.toString());
				}
			}
		}
		
	}
	
	//order the relations
	private void arrangeRelations(){

		initialOrderedLabel();	
		
		//add all labels related with a construction
		for(int i = 0; i < objectTable.getRowCount();i++){
			//advanced points are viewed as relations
			if(objectTable.getInt(i,"role")>1){
				Structure4Ordering relation = new Structure4Ordering(objTab, i, labelCount);
				relation.labelList[orderedReference.get(objectTable.getString(i, "reference"))] = true;
				Vector<String> labels = getLabelsOfGeobject(objectTable.getString(i, "geobject"));
				
				for(int j = 0; j < labels.size(); j++){
					//System.out.println(labels.get(j));
					relation.labelList[orderedReference.get(labels.get(j))] = true;
				}
				relationList.add(relation);
			}
		}
		
		//print();
		
		for(int i = 0; i < constraintTable.getRowCount();i++){
			//advanced points are viewed as relations
			if(constraintTable.getInt(i,"role")>0){
				Structure4Ordering relation = new Structure4Ordering(conTab, i, labelCount);
				Vector<String> labels = getLabelsOfGeobject(constraintTable.getString(i, "geobject"));
				for(int j = 0; j < labels.size(); j++){
					System.out.println(labels.get(j));
					relation.labelList[orderedReference.get(labels.get(j))] = true;
				}
				relationList.add(relation);
			}
		}
		
		for(int t = 0; t < relationList.size(); t++){
			relationList.get(t).print();
		}
		
		//order relations strategy : back-first
//		for(int j = relationList.size(); j >0 ; j--){
//			int toLast = -1;
//			for(int i = labelCount; i >0; i--){
//				for(int t = 0; t < j; t++){
//				
//					if(relationList.get(t).labelList[i-1]==true){
//						//there is one 
//						if(toLast == -1){
//							toLast = t;
//						}else{
//							//there are two lines of true
//							toLast = selectToLast(relationList.get(toLast).labelList, toLast, relationList.get(t).labelList, t, i-1);
//						}
//					}
//				}
//				if(toLast!=-1){
//					Structure4Ordering buf = relationList.get(toLast);
//					relationList.remove(toLast);
//					relationList.insertElementAt(buf, j-1);
//					break;
//				}
//			}
//			System.out.println("move " + j + "============================");
//			for(int t = 0; t < relationList.size(); t++){
//				relationList.get(t).print();
//			}
//
//		}
		
		//order relations strategy: front-first
		for(int j = 0 ; j < relationList.size()-1 ; j++){
			int toFirst = -1;
			for(int i = 0; i < labelCount; i++){
				for(int t = j; t < relationList.size(); t++){
				
					if(relationList.get(t).labelList[i]==true){
						//there is one 
						if(toFirst == -1){
							toFirst = t;
						}else{
							//there are two lines of true
							toFirst = selectToFirst(relationList.get(toFirst).labelList, toFirst, relationList.get(t).labelList, t, i);
						}
					}
				}
				if(toFirst!=-1){
					Structure4Ordering buf = relationList.get(toFirst);
					relationList.remove(toFirst);
					relationList.insertElementAt(buf, j);
					break;
				}
			}
			System.out.println("move " + j + "============================");
			for(int t = 0; t < relationList.size(); t++){
				relationList.get(t).print();
			}

		}
		
		
		System.out.println(orderedReference);

		System.out.println("============================");
		for(int t = 0; t < relationList.size(); t++){
			relationList.get(t).print();
		}
	}
	
	private int selectToFirst(boolean[] a, int aNum, boolean[] b, int bNum, int length){
		int result = -1;
		if(length<labelCount){
			if(a[length]== b[length]){
				result = selectToFirst(a, aNum, b, bNum, length+1);
			}else
				if(a[length]==true && b[length]==false){
					result = aNum;
				}else
					if(a[length]==false && b[length]==true){
						result = bNum;
					}
		}
		
		return result;
	}
	
	private int selectToLast(boolean[] a, int aNum, boolean[] b, int bNum, int length){
		int result = -1;
		if(length>=0){
			if(a[length]== b[length]){
				result = selectToLast(a, aNum, b, bNum, length-1);
			}else
				if(a[length]==true && b[length]==false){
					result = aNum;
				}else
					if(a[length]==false && b[length]==true){
						result = bNum;
					}
		}
		
		return result;
	}
	
	
	private Vector<String> getLabelsOfGeobject(String obj){
		//System.out.println(obj);
		Vector<String> result = new Vector<String>(1,1);
		if(obj!=null){
			Vector<String> attr = Utility.generateTermSet(obj);
			for(int i = 1; i < attr.size(); i++){
				if(attr.get(i).indexOf("(")!=-1){
					result.addAll(getLabelsOfGeobject(attr.get(i)));
				}else{
					result.add(attr.get(i));
				}
			}
		}
		
		return result;
	}
	
	
	//initial the orderedReference
	private void initialOrderedLabel(){
		Vector<Integer> labelCounts = new Vector<Integer>(1,1);
		//the order of references depend on the point counts
		for(int m = 0; m < objectTable.getRowCount(); m++){
			if(objectTable.getInt(m,"role")>0){
				labelCounts.add(objectTable.getInt(m, "pointCount"));
			}else{
				labelCounts.add(-10);
			}
		}
		
		
		//revise the labelCounts by adapting the construction  
		Hashtable<String,Integer> tab = new Hashtable<String,Integer>(1,1);
		Vector<String[]> dependencies = new Vector<String[]>(1,1);
		for(int m = 0; m < objectTable.getRowCount(); m++){
			if(objectTable.getInt(m,"role")>0){
				if(!tab.containsKey(objectTable.getString(m, "reference"))){
					tab.put(objectTable.getString(m, "reference"),objectTable.getInt(m, "pointCount"));
				}
				if(objectTable.getInt(m, "role")>1){
					String pre = objectTable.getString(m, "reference");
					Vector<String> subs = this.getLabelsOfGeobject(objectTable.getString(m, "geobject"));
					for(int t = 0; t < subs.size(); t++){
						if(!pre.equals(subs.get(t))){
							dependencies.add(new String[]{pre,subs.get(t)});
						}
					}
				}
			}
		}
//		for(int n = 0; n < constraintTable.getRowCount(); n++){
//			if(constraintTable.getInt(n, "role")>0){
//				String pre = constraintTable.getString(n, "attribute1");
//				Vector<String> subs = this.getLabelsOfGeobject(constraintTable.getString(n, "attribute2"));
//				for(int t = 0; t < subs.size(); t++){
//					if(pre.indexOf("(")==-1&&!pre.equals(subs.get(t))){
//						dependencies.add(new String[]{pre,subs.get(t)});
//					}
//				}
//			}
//		}
		
		reviseLabelCounts(tab, dependencies);
		
		for(int m = 0; m <labelCounts.size(); m++){
			if(tab.containsKey(objectTable.getString(m, "reference"))){
				labelCounts.set(m, tab.get(objectTable.getString(m, "reference")));
			}
		}
		
		
		
		int currentIndex = -1;
		int currentMaxCount = -10;
		int order = 0;
		for(int i = 0; i < labelCounts.size(); i++){
			currentIndex = -1;
			currentMaxCount = -10;
			for(int p = 0; p < labelCounts.size(); p++){
				//deal with the case there are repeated labels 
					if(labelCounts.get(p) > currentMaxCount){
							currentMaxCount = labelCounts.get(p);
							currentIndex = p;
					}
			}
			if(currentIndex == -1){
				break;
			}else{
				if(orderedReference.containsKey(objectTable.getString(currentIndex,"reference"))){
					labelCounts.set(currentIndex,-10);
				}else{
					orderedReference.put(objectTable.getString(currentIndex,"reference"), order);
					labelCounts.set(currentIndex,-10);
					order++;
					labelCount++;
				}
			}
		}
	}
	
	
	private void reviseLabelCounts(Hashtable<String,Integer> labelCounts, Vector<String[]> dependencies){
		for(int i = 0; i < dependencies.size(); i++){
			String[] currentDependency = dependencies.get(i);
			if(labelCounts.get(currentDependency[0])>=labelCounts.get(currentDependency[1])){
				labelCounts.put(currentDependency[0], labelCounts.get(currentDependency[0])-1);
				reviseLabelCounts(labelCounts, dependencies);
			}
		}
	}
	
	
	
	//According to the order of relations, filter theorems, and then generate theorems
//	private void generateTheorem(){
//		
//		
//		arrangeRelations();
//
//		
//		Vector<String> objects = new Vector<String>(1,1);
//		for(int i = 0 ; i < objectTable.getRowCount(); i++){
//			if(objectTable.getInt(i, "role")==1){
//				String str = objectTable.getString(i, "reference")+":="+objectTable.getString(i, "geobject");
//				objects.add(str);
//			}
//		}
//		
//		for(int i = relationList.size(); i > 0; i--){
//			//select a relation to be conclusion
//			//the conclusion only contains existing labels 
//			Structure4Ordering currentR = relationList.get(i-1);
//			boolean[] currentL = currentR.labelList;
//			boolean currentCanBe = true;
//			for(int k = 0; k < currentL.length; k++){
//				if(currentL[k]==true){
//					boolean test = false;
//					for(int m = 0; m < relationList.size(); m++){
//						if(m!=i-1){
//							test = test || relationList.get(m).labelList[k];
//						}
//					}
//					if(!test){
//						currentCanBe = false;
//					}
//				}
//			}
//			
//			//heuristics for the conclusions
//			/*
//			 * if an object is already constructed in the objectTable, then it can not be a conclusion unless there 
//			 * are more than one constructions about the object
//			 */
//			if(currentR.tableName==objTab){
//				String label = objectTable.getString(currentR.rowInTable,"reference");
//				Vector<Integer> list = automatica.Utility.getRowNumList(objectTable, label, "reference");
//				if(list.size()<=1){
//					currentCanBe = false;
//				}
//			}
//			
//			
//			if(currentCanBe){
//				StringBuffer theorem = new StringBuffer(1);
//				theorem.append("Problem(" + name +(i)+",Theorem,assume(");
//				for(int k = 0; k < objects.size(); k++){
//					theorem.append(objects.get(k)+",");
//				}
//				for(int j = 0; j < relationList.size(); j++){
//					if(j!=i-1){
//						Structure4Ordering so = relationList.get(j);
//						if(so.tableName==objTab){
//							theorem.append(objectTable.getString(so.rowInTable, "reference")+":="+objectTable.getString(so.rowInTable, "geobject")+",");
//						}else
//							if(so.tableName==conTab){
//								theorem.append(constraintTable.getString(so.rowInTable, "geobject")+",");
//							}
//					}
//				}
//				
//				String conclusion = "";
//				Structure4Ordering conso = relationList.get(i-1);
//				if(conso.tableName==objTab){
//					if(objectTable.getInt(conso.rowInTable, "role")==2)
//					conclusion = "is("+objectTable.getString(conso.rowInTable, "reference")+","+objectTable.getString(conso.rowInTable, "geobject")+")";
//				}else
//					if(conso.tableName==conTab){
//						conclusion = constraintTable.getString(conso.rowInTable, "geobject")+",";
//					}
//				
//				theorem.replace(theorem.lastIndexOf(","), theorem.length(), "),show("+conclusion+"))");
//				
//				if(filterTheorem(theorem.toString())!=null){
//					theorems.add(theorem.toString());
//				}
//			}
//		}
//		
//	}
	
	private String filterTheorem(String theorem){
		//use algebraic computation and numerical computation to test the truth of a theorem
		String result = theorem;
		
		//heuristic rules for ordering predicates
		//initialOrderedReference();
		
//		Vector<String> l = getLabelsOfGeobject("h(ff(A,B,C),fa(A,B))");
//		for(int i = 0; i < l.size(); i++){
//			System.out.println(l.get(i));
//		}
		
		//System.out.println("hellofadfa" + orderedReference);
		
		//determine arbitrary points for the theorem
		
		
		//assign coordinates and compute triangular set
		
		
		//assign random values in u and determine the values of other coordinates
		
		
		//check whether the conclusion holds. If not, kick off the theorem from candidates
		
		
		return result;
		
	}
	

	
	
	private void packageTheorem(String path){
		StringBuffer output = new StringBuffer(1);
		output.append("Problems(");
		for(int i = 0; i < theorems.size(); i++){
			//System.out.println(theorems.get(i));
			output.append(theorems.get(i)+",");
		}output.replace(output.lastIndexOf(","), output.length(), ")");
		
		Utility.saveFile(null, output.toString(), new File(path.replace("_GDL", "Theorems")));
	}
	
	

	
	private class Structure4Ordering{
		Structure4Ordering(int tableName, int rowInTable, int labelSize){
			this.tableName = tableName;
			this.rowInTable = rowInTable;
			this.labelList = new boolean[labelSize];
			for(int i = 0; i < labelSize; i++){
				labelList[i] = false;
			}
		}
		
		void print(){
			System.out.print(tableName + " " + rowInTable + " : ");
			for(int i = 0; i < labelList.length; i++){
				System.out.print(labelList[i] + " ");
			}
			System.out.print("\n");
		}
		
		private int tableName;
		private int rowInTable;
		private boolean[] labelList;
		
	}
	
	private Table objectTable = new Table();
	private Table constraintTable = new Table();
	private Hashtable<String, Integer> orderedReference = new Hashtable<String, Integer>();
	private Vector<String> theorems = new Vector<String>(1,1);
	private int objTab = 0;
	private int conTab = 1;
	private int labelCount = 0;
	private Vector<Structure4Ordering> relationList = new Vector<Structure4Ordering>(1,1);
	private String name;
	private String fileLocate = "E://360Cloud/Program/GeoTransformer/examples/geoRecognizer/experiments/";

}
